\documentclass[a4paper,10pt]{article}
\usepackage[utf8x]{inputenc}
\usepackage[english]{babel}
\usepackage{xspace}
\usepackage{float}
\usepackage{amstext, amssymb, amsfonts, amsmath}
%\usepackage{amsthm}
\usepackage{latexsym}
\usepackage{stmaryrd}
\usepackage{float}
\usepackage{graphicx}
\usepackage{geometry}
\usepackage{enumerate}
\usepackage{times}
\usepackage{color}
\usepackage{url}
\usepackage{hyperref}


\usepackage{macron}

%opening
\title{Enhanced process abstractions for \\ runtime session adaptation}
\author{Cinzia Di Giusto \and Jorge A. Pérez}
\date{Proposal for a BETTY STSM in Lisbon, August 2013}

\begin{document}

\maketitle

\begin{abstract}
%In this STSM we plan to extend and discuss previous works on behavioral types for adaptable systems.
%We refer to adaptable models every time we deal with  systems that require to be upgraded without being stopped. For these systems we have proposed a session types discipline that regulates the  communication between partners in such a way that no protocol is interrupted by a careless adaptation routine. 
%In previous informal discussions we have identified some possible extensions to this work: in particular we would like to update a process even if it contains some already open sessions. This operation should ensure that the communication protocol is not interrupted, thus keeping the consistency with the partners.  
%
%We propose one-week STSM in Lisbon, Portugal, during which we would characterize some of the ideas hinted at above. At the end of the week, we should be able to have a first draft to be developed in subsequent on line   meetings with the aim of a conference submission to forthcoming top venues.

We propose a one-week STSM in Lisbon, Portugal
to continue an ongoing collaboration on typed process abstractions for adaptable communicating systems.
Such systems are increasingly common in practice, and yet theories of behavioral types for ensuring their correctness need further work. Our approach focuses on developing a solid understanding of process abstractions for adaptation, as a way of ensuring their effective integration with type disciplines for binary and multiparty session types.


More in details, we plan to extend our previous works on behavioral types for adaptable systems. Our current discipline extends
binary session types to enforce a static control over communicating partners, in such a way that no protocol is interrupted by a careless adaptation routine. A limitation of this framework is that adaptation is defined only for processes without open sessions. In this STSM we plan to investigate how to overcome this limitation, in such a way that more flexible and expressive adaptation routines can be modeled and reasoned about with appropriate behavioral type theories. We aim at formally defining an enhanced update operation which ensures that the communication protocol is not interrupted, thus keeping the consistency with the partners. In preliminary investigations, we have discovered that the aimed flexibility may be achieved by integrating event-based typed constructs, as proposed recently by Kouzapas et al. So in the STSM we wish to develop further such investigations; at the end of the STSM, we should have a first draft of a conference submission to forthcoming top venues.




\end{abstract}




We have recently proposed the concept of \emph{adaptable processes}~\cite{BGPZFMOODS}: this is a process abstraction 
intended to 
model all those scenarios that concern forms of dynamic process evolution. 
This notion finds an application in those contexts where systems require to be updated without being stopped. An update can either be the result of a developer upgrade (say, bug fixing or adding new features) or it can be the outcome of an adaptation to unexpected circumstances 
(say, changes in underlying platforms, resource availability, or user demand).

%In order to implement this idea, a
Adaptable processes have a location and are sensible to actions of dynamic update at runtime. 
Localities allow to conceptually organize the behavior and provide a way for referring to such behavior; they may be seen as analogous to 
modules/classes in object-oriented programs. Located behavior may be modified at runtime by means of 
an update operator.
% permits to change the code of a ``working unit''.
More precisely, given a location (name) $l$, a process $P$, and a context $Q(\mathsf{X})$ 
(i.e. a process $Q$ with free occurrences of variable $\mathsf{X}$), located processes and update operators are noted $l[P]$ and 
$\adapt{l}{Q}{X}$, respectively. 
%$l\{Q(\mathsf{X})\}$, resp. 
These two processes may synchronize on $l$ so as to evolve into process 
$Q\subst{P}{\mathsf{X}}$ ---the process $Q$ in which all free occurrences of $X$ are replaced with $P$.
This interaction represents the \emph{update} of  process $P$ at $l$ with an \emph{adaptation routine}
(or built-in adaptation mechanism)
embodied by $Q(\mathsf{X})$. Locations can be nested and are transparent:
within $l[P]$, process $P$ may evolve autonomously, with the potential of interacting with some neighboring 
update process for $l$. 
%$l\{Q(\mathsf{X})\}$, 
%$\adapt{l}{Q}{X}$,
%as just described,
 
We have considered located processes and update operators in the context 
of variants of CCS and the $\pi$-calculus. Hence, in the resulting process languages,
interactive, communicating behavior coexists with update actions. 
The interplay of both forms of interaction results in an expressive and powerful tool, which begs for some form of static control.
At a high-level, we would like to offer modelers and developers mechanisms for ensuring that correct communications (as guaranteed by tools based upon behavioral types and contracts)
are not compromised by update/reconfiguration actions.
%This is why some ``automatic ways'' of supporting the developer work  should be introduced. 
A first attempt in this direction is our work in~\cite{DBLP:conf/sac/GiustoP13,Places13}, where we have proposed a session types discipline that regulates the  communication between partners in such a way that no protocol is interrupted by a careless adaptation routine: i.e., 
update actions over located processes
which are engaged in active session behavior cannot be enabled.

In the proposed STSM, we plan to explore more flexible mechanisms for statically controlling reconfiguration actions, in a session-typed setting.
%This is a quite rigid way to control updates, indeed an update can be indefinitely delayed by a protocol that continuously establishes new sessions. Thus, it would be interesting of finding more flexible ways of controlling updates. This is what we plan to investigate during the STSM.
In particular, we plan to extend our previous works by  considering a different (finer) level of granularity: we would like to be able to update a located process even if it contains some already open sessions. 
To this end, we plan to investigate an extension of our framework with the \texttt{typecase} operator recently proposed by Kouzapas et al~\cite{Kouzapas12}. This should be useful to know the current protocol state at a single session, and to define an appropriate reconfiguration routine for such a state.
Such a routine should contain (or define) a ``wrapper'' or adaptor process, which should ensure that 
(a) already established sessions are treated seamlessly, and (b) the given session is indeed updated for the rest of the protocol. 
%This should be obtained by introducing a new operator that can test types and by building proper wrappers that 1) preserve already established sessions but 2) update the  behavior of the unit for future sessions.

Overall, the proposed STSM should result in a concrete basis for future developments, to be carried out remotely, with the aim of a conference submission to forthcoming top venues, such as, e.g., ESOP'14. It should also be very useful to clarify the intrinsic nature of adaptable processes in more sophisticated settings, such as multiparty sessions. Indeed, we expect the results of the proposed STSM could be transferred to enrich ongoing efforts on multiparty adaptation. 

\bibliographystyle{abbrv}
\bibliography{referen}



\end{document}
